#include "PDTNode.h"

#include "PDTZ3GraphVisitor.h"

#include "PDTNumVar.h"
#include "PDTNumConst.h"
#include "PDTBoolVar.h"
#include "PDTBoolConst.h"
#include "PDTFunction.h"
#include "PDTProp.h"

/*
 Constructor of Z3 Visitor
 */
PDTZ3Visitor::PDTZ3Visitor(PDTCodeGraph & aCG) :
  counter(0), boundCounter(0),
  prepQuant(aCG.maxWhileDepth),
  CG(aCG)
{
  // call setup function to create a context and 
  // declare the necessary
  // structures and functions
  setup();

  // build Z3 nodes for variables and constants
  // start with them since they are at the bottom of
  // the parse DAG
  for (unsigned int i = 0; i < CG.variables.size(); i++)
    {
      PDTNode * var = CG.variables[i]->getNode();
      var->Z3visit(*this);
    }
  for (unsigned int i = 0; i < CG.constants.size(); i++)
    {
      PDTNode * constant = CG.constants[i]->getNode();
      constant->Z3visit(*this);
    }
#if 0

  current = Start;

  // visit all top nodes. 
  // that is all nodes with no parents.
  for (unsigned int i = 0; i < CG.nodes.size(); i++)
    {
      PDTNode * node = CG.nodes[i];

      /* taverse the top level nodes to keep track of the correct while depth */
      if (node->getParents().size() == 0)
          node->Z3visit(*this);
    }
#endif
}

PDTZ3Visitor::Sat_Em
PDTZ3Visitor::check() 
{ //TODO:
    Z3_lbool check = Z3_check(ctx);
    if (check == Z3_L_TRUE){
        cout << "Check is satisfiable "<< endl;
        return Sat;
    }
    if (check == Z3_L_FALSE) {
        cout << "Check is not satisfiable "<< endl;
        return Unsat;
    }
    cout <<"check is undefined"<< endl;
    return None;
}

void
PDTZ3Visitor::toString() 
{
    cout << "calling toString " << endl;
    Z3_string str = Z3_context_to_string(ctx);
    cout << "Z3 context string follows." << endl;
    cout << str << endl;
}

PDTZ3Visitor::~PDTZ3Visitor()
{
  Z3_del_context(ctx);

  delete[] ArrayOfStatements;
  delete [] eOrder; 
  delete [] InGamma;
  delete [] s2i;
}


/*
 * buildTypesAndConstants() declares the needed Z3 sorts:
 * Int, Bool, Statement, and Var.
 * It also declares constants needed across the translation:
 * Zero, True, False, Start and Infinity.
 */
void
PDTZ3Visitor::buildTypesAndConstants()
{
  Int = Z3_mk_int_sort(ctx);
  Bool = Z3_mk_bool_sort(ctx);

  True = Z3_mk_true(ctx);
  False = Z3_mk_false(ctx);
  Zero = Z3_mk_int(ctx, 0, Int);

  //(declare-sort Statement 0)
  Z3_symbol StatementName = Z3_mk_string_symbol(ctx, "Statement");
  Statement = Z3_mk_uninterpreted_sort(ctx, StatementName);

  ArrayOfStatements = new Z3_sort[CG.maxWhileDepth+1];
  makeArrayOfStatementsSort(CG.maxWhileDepth);

  /*
(declare-fun Start () Statement)      
(declare-fun Infinity ()  Statement)   
   */
  Start = makeStatement("Start");
  Z3_symbol fStartName = Z3_mk_string_symbol(ctx, "fStart");
  fStart = Z3_mk_func_decl(ctx, fStartName, 0, NULL, Statement);
  Z3_ast fStartApply = Z3_mk_app(ctx, fStart, 0, NULL);
  Z3_ast startEQfStart = Z3_mk_eq(ctx, fStartApply, Start);
  Z3_assert_cnstr(ctx, startEQfStart);

  Infinity = makeStatement("Infinity");
  Z3_symbol fInfinityName = Z3_mk_string_symbol(ctx, "fInfinity");
  fInfinity = Z3_mk_func_decl(ctx, fInfinityName, 0, NULL, Statement);
  Z3_ast fInfinityApply = Z3_mk_app(ctx, fInfinity, 0, NULL);
  Z3_ast startEQfInfinity = Z3_mk_eq(ctx, fInfinityApply, Infinity);
  Z3_assert_cnstr(ctx, startEQfInfinity);

//(declare-sort Var 0)
  Z3_symbol VarName = Z3_mk_string_symbol(ctx, "Var");
  Var = Z3_mk_uninterpreted_sort(ctx, VarName);

//(declare-fun IV (Var) Int)  
  Z3_symbol IVName = Z3_mk_string_symbol(ctx, "IV");
  Z3_sort IVDomain[1];
  IVDomain[0] = Var;
  IV = Z3_mk_func_decl(ctx, IVName, 1, IVDomain, Int);
}

/*
 * Declare the function that maps a statement to its execution time expressed as an Int
 */
void
PDTZ3Visitor::declareExecutionTimeFunction()
{
  Z3_symbol EName;
  Z3_sort EDomain[1];
/*
(declare-fun E (Statement) Int)
*/
  EName = Z3_mk_string_symbol(ctx, "E");
  EDomain[0] = Statement;
  E = Z3_mk_func_decl(ctx, EName, 1, EDomain, Int);

//(assert (= (E Start) 0))
  Z3_ast eStart1 = mk_unary_app(ctx, E, Start);
  Z3_ast eStartEqZero = Z3_mk_eq(ctx, eStart1, Zero);
  Z3_assert_cnstr(ctx, eStartEqZero);

//(assert (< (E Start) (E Infinity)))
  Z3_ast eStart2 = mk_unary_app(ctx, E, Start);
  Z3_ast eInfinity = mk_unary_app(ctx, E, Infinity);
  Z3_ast eStartLTeInfinity = Z3_mk_lt(ctx, eStart2, eInfinity);
  Z3_assert_cnstr(ctx, eStartLTeInfinity);


  eOrder = new Z3_func_decl[CG.maxWhileDepth+1];

  for (unsigned int i = 0; i < CG.maxWhileDepth+1; i++)
    {
      char eOrderString[10];
      sprintf(eOrderString, "eOrd%d", i);

      Z3_symbol eOrderName = Z3_mk_string_symbol(ctx, eOrderString);
      Z3_sort eOrderDomain[2];
      eOrderDomain[0] = ArrayOfStatements[i];
      eOrderDomain[1] = ArrayOfStatements[i];
      eOrder[i] = Z3_mk_func_decl(ctx, eOrderName, 2, eOrderDomain, Bool);
      if (i == 0)
        continue;
      /* 
       now assert that eOrder[I](s1,s2) <=> forall j eOrder[I-1](s1[j], s2[j])

       (define-fun eOrderI ( (s1 statementI) (s2 statementI)) bool
       (forall (i Int) ( eOrderI-1 (select s1 i) (select s2 i)    )
       ) )
       */
#if 0
      const char * funcDefTemp = "(benchmark cg2z3 :formula "
        "(define-fun eOrd%d ( (s1 %s) (s2 %s)) Bool "
        " (forall (i Int) ( eOrd%d (select s1 i) (select s2 i) ) ) ) )";
#else
      const char * funcDefTemp = "(benchmark cg2z3 :formula "
        "(forall (s1 %s) (s2 %s)  (= (eOrd%d s1 s2) "
        " (forall (i Int) ( eOrd%d (select s1 i) (select s2 i) ) ) ) ) )";
#endif
      char funcDef[1024];
      /*
       Z3_string Z3_API    Z3_get_symbol_string (__in Z3_context c, __in Z3_symbol s)*/

      const char * aSI = Z3_sort_to_string(ctx, ArrayOfStatements[i]);
#if 0
      const char * aSIMinus = Z3_sort_to_string(ctx, ArrayOfStatements[i - 1]);
      sprintf(funcDef, funcDefTemp, i, aSI, aSIMinus, i - 1);
#else
      sprintf(funcDef, funcDefTemp, aSI, aSI, i, i - 1);
#endif

      Z3_sort sorts[4] = { ArrayOfStatements[i - 1], ArrayOfStatements[i], Bool, Int};
      Z3_func_decl decls[2] = { eOrder[i], eOrder[i - 1]};
      Z3ParseSMTLibString(funcDef, 3, sorts, 2, decls, "eOrd");
    }
  // assert that eOrd[0](s1,s2)  == E(s1) < E(s2)
#if 0
  const char * funcDef = "(benchmark aaa :formula "
      "(define-fun eOrd0 ( (s1 Statement) (s2 Statement)) Bool "
      "(< (E s1) (E s2))))";
#else
  const char * funcDef = "(benchmark aaa :formula "
      "(forall (s1 Statement) (s2 Statement) ( = (eOrd0 s1 s2)  "
      "(< (E s1) (E s2) ) ) ) )";
#endif

    Z3_sort sorts[3]= { Statement, Bool, Int};
    Z3_func_decl decls[2] = { eOrder[0], E};
    Z3ParseSMTLibString(funcDef, 2, sorts, 2, decls, "eOrd0");
}

Z3_ast
PDTZ3Visitor::Z3ParseSMTLibString(const char * funcDef, unsigned int nSorts,
    Z3_sort sorts[], unsigned int nDecls, Z3_func_decl decls[],
    const char * funcName)
{
  if (funcName == NULL)
    funcName = funcDef;

  Z3_symbol * sNames = new Z3_symbol[nSorts];

  for (unsigned int i = 0; i < nSorts; i++)
    {
      sNames[i] = Z3_get_sort_name(ctx, sorts[i]);
    }

  Z3_symbol * dNames = new Z3_symbol[nDecls];
  for (unsigned int i = 0; i < nDecls; i++)
    {
      dNames[i] = Z3_get_decl_name(ctx, decls[i]);
    }

  Z3_parse_smtlib_string(ctx, funcDef,
      nSorts, sNames, sorts,
      nDecls, dNames, decls);
  unsigned rc = Z3_get_smtlib_num_formulas(ctx);
  if (rc < 1)
    {
      cerr << "Error: Z3 did not parse " << funcDef << " correctly" << endl;
      exit(0);
    }
  assert (rc == 1);
  Z3_ast def = Z3_get_smtlib_formula(ctx, 0);
  Z3_assert_cnstr(ctx, def);

  delete[] sNames;
  delete[] dNames;

  return def;
}

/*
 * InGamma is a function that maps a tuple (v: Var, s: Statement) to true is s is an 
 * assignment statement that affects v, and to false otherwise.  
 */
void
PDTZ3Visitor::declareInGamma()
{

  InGamma = new Z3_func_decl[CG.maxWhileDepth+1];

  for (unsigned int i = 0; i < CG.maxWhileDepth+1; i++){
    const char * nameT = "inGamma%d";
    char name[10];
    sprintf(name, nameT, i);

    Z3_symbol G_name;
    G_name = Z3_mk_string_symbol(ctx, name);

    Z3_sort G_domain[2];
    G_domain[0] = Var;
    G_domain[1] = ArrayOfStatements[i];

    InGamma[i] = Z3_mk_func_decl(ctx, G_name, 2, G_domain, Bool);
    if ( i == 0)
        continue;
      /* 
       now assert that inGamma[i](s,v) <=> forall j inGamma[i-1](s[j], v) 
       */
#if 0
      const char * funcDefTemp = "(benchmark cg2z3 :formula"
        "(define-fun inGamma%d ( (v Var) (s %s) ) bool"
        "(forall (i Int) ( inGamma%d v (select s i) ) ) ) )";
#else
      const char * funcDefTemp = "(benchmark cg2z3 :formula "
        "(forall (v Var) (s %s) (= (inGamma%d v s) "
        "(forall (i Int) ( inGamma%d v (select s i) ) ) ) ) )";
#endif
      char funcDef[1024];

      const char * aSI = Z3_sort_to_string(ctx, ArrayOfStatements[i]);
#if 0
      sprintf(funcDef, funcDefTemp, i, aSI, i - 1);
#else
      sprintf(funcDef, funcDefTemp, aSI, i, i - 1);
#endif

      Z3_sort sorts[4];
      sorts[0] = ArrayOfStatements[i - 1];
      sorts[1] = ArrayOfStatements[i];
      sorts[2] = Var;
      sorts[3] = Bool;

      Z3_func_decl decls[2];
      decls[0] = InGamma[i-1];
      decls[1] = InGamma[i];

      Z3ParseSMTLibString(funcDef, 4, sorts, 2, decls, "inGamma");
  }
  {
      /*
(assert (forall (v Var) 
         (and 
         (not (inGamma0 v Start)) (not (inGamma0 v Infinity)))))
         */
#if 0
      Z3_ast v = Z3_mk_bound(ctx, 0, Var);
      Z3_ast inGVStart = mk_binary_app(ctx, InGamma[0], v, Start);
      Z3_ast inGVInfinity = mk_binary_app(ctx, InGamma[0], v, Infinity);
      Z3_ast notInGVStart = Z3_mk_not(ctx, inGVStart);
      Z3_ast notInGVInfinity = Z3_mk_not(ctx, inGVInfinity);
      Z3_ast args[2] = {notInGVStart, notInGVInfinity};
      Z3_ast body = Z3_mk_and(ctx, 2, args);

      Z3_sort sorts[1];
      sorts[0] = Var;

      Z3_symbol names[1];
      names[0] = Z3_mk_string_symbol(ctx, makeName("v"));

      Z3_ast constraint = Z3_mk_forall(ctx,0,0,0,//patterns!
              1, sorts, names, body);
      Z3_assert_cnstr(ctx, constraint);
#else
      const char * excludeStartInfinity = "(benchmark cg2z3 :formula "
          "(forall (v Var) (and "
          " (not (inGamma0 v (fStart)))  "
          " (not (inGamma0 v (fInfinity))) ) ) )";

      Z3_sort sorts[3] = {Var, Statement, Bool };
      Z3_func_decl decls[3] = { InGamma[0], fStart, decls[2] = fInfinity };
      Z3ParseSMTLibString(excludeStartInfinity, 3, sorts, 3, decls, "inGamma0");
#endif
  }
}

/*
 * Val (v: Var, t: Int) -> s: Statement
 * Val is a function that picks and returns s, one of the assignment statements
 * that assign values to v.  
 * Val picks s so that the execution time of s is the most recent wrt to the time t.  
 */
void
PDTZ3Visitor::declareAndDefineVal()
{
  /*
   VAL takes variable and current time and returns the most recent statement that affects the variable's value

   (declare-fun VAL (Var Int) statement)
(assert (forall (s Statement) (v Var) 
         (=> (and (> (E s) (E Start)) (<= (E s) (E Infinity)) ) 
          (isMaxBefore v s (VAL v (E s))))))
   */
  Z3_symbol VAL_name = Z3_mk_string_symbol(ctx, "VAL");

  Z3_sort VAL_domain[2];
  VAL_domain[0] = Var;
  VAL_domain[1] = Int;
  VAL = Z3_mk_func_decl(ctx, VAL_name, 2, VAL_domain, Statement);

  /*	implementation	*/
  /*
(assert (forall (s Statement) (v Var) 
         (=> (and (> (E s) (E Start)) (<= (E s) (E Infinity)) ) 
          (isMaxBefore v s (VAL v (E s))))))

   this means that the value of variable v that 
   we can use to evaluate statement s is the
   last statement that assigns to v that was executed
   before s. 
   */
  Z3_symbol sName;
  Z3_ast s = makeBound(Statement,sName);

  Z3_ast eS1 = mk_unary_app(ctx, E, s);
  Z3_ast eStart = mk_unary_app(ctx, E, Start);
  Z3_ast esGTstart = Z3_mk_gt(ctx, eS1, eStart);

  Z3_ast eS2 = mk_unary_app(ctx, E, s);
  Z3_ast eInfinity = mk_unary_app(ctx, E, Infinity);
  Z3_ast esLEinfinity = Z3_mk_le(ctx, eS2, eInfinity);

  Z3_ast args[2]; 
  args[0] = esGTstart;
  args[1] = esLEinfinity;
  Z3_ast sRange = Z3_mk_and(ctx, 2, args);

  Z3_symbol vName; 
  Z3_ast v = makeBound(Var, vName);
  Z3_ast eS3 = mk_unary_app(ctx, E, s);
  Z3_ast valVS = mk_binary_app(ctx, VAL, v, eS3);

  Z3_ast isMaxBeforeArgs[3];
  isMaxBeforeArgs[0] = v;
  isMaxBeforeArgs[1] = s;
  isMaxBeforeArgs[2] = valVS;

  Z3_ast isMaxBeforeApply = Z3_mk_app(ctx, isMaxBefore, 3, isMaxBeforeArgs);

  Z3_ast implies = Z3_mk_implies(ctx, sRange, isMaxBeforeApply);

  Z3_sort sorts[2] = {Statement, Var};
  Z3_symbol names[2] = {sName, vName};

  Z3_ast constraint = Z3_mk_forall(ctx,0,0,0,//TODO: add patterns!
      2, sorts, names, implies);
  Z3_assert_cnstr(ctx, constraint);
}

char *
PDTZ3Visitor::makeName(const char * prefix, int i)
{
  static char name[1024];
  static int counter = 100;
  if (i != 0)
    {
      /*
       * TODO: If i != 0 then include i in the name
       */
    }
  sprintf(name, "CG_%s_CNT_%d", prefix, counter);
  counter++;
  return name;
}

/*
 * isMaxBefore is a priority encoder
 * isMaxBefore : ( v: var, sS: Statement, sT: Statement) -> Bool
 * it returns true in case sT is the most recent statement that updates variable v
 * before statement sS.
 * The order here is the execution order of the statements.  
 */
void
PDTZ3Visitor::declareAndDefineIsMaxBefore()
{
  /*
   ;isMaxBefore returns true if sT is the most recent statement updating v before sS
(define-fun isMaxBefore ((v Var) (sS Statement) (sT Statement)) Bool
          (and (< (E sT) (E Infinity))
               ( or (= sT Start) (inGamma0 v sT))
               (< (E sT) (E sS))
               (forall (s Statement) (=>                                
                      (inGamma0 v s)
                      (=> (< (E s) (E sS)) (<= (E s) (E sT)) ) )
                  :pattern ((inGamma0 v s) (< (E s) (E sS)))
) ) )
   */
  Z3_symbol sym = Z3_mk_string_symbol(ctx, "isMaxBefore");

  Z3_sort domain[3]={Var, Statement, Statement};
  isMaxBefore = Z3_mk_func_decl(ctx, sym, 
          3, domain, Bool);

#if 0
  const char * funcDef = "(benchmark cg2z3 :formula "
"(define-fun isMaxBefore ((v Var) (sS Statement) (sT Statement)) Bool "
"          (and (< (E sT) (E Infinity)) "
"               ( or (= sT Start) (inGamma0 v sT)) "
"               (< (E sT) (E sS)) "
"               (forall (s Statement) (=>  "
"                      (inGamma0 v s) "
"                      (=> (< (E s) (E sS)) (<= (E s) (E sT)) ) ) "
"                  :pattern ((inGamma0 v s) (< (E s) (E sS))) "
") ) ) ";
#else
  const char * funcDef = "(benchmark cg2z3 :formula "
    "(forall (v Var) (sS Statement) (sT Statement) "
    "(= (isMaxBefore v sS sT) "
"          (and (< (E sT) (E (fInfinity) )) "
"               ( or (= sT (fStart) ) (inGamma0 v sT)) "
"               (< (E sT) (E sS)) "
"               (forall (s Statement) (implies "
"                      (inGamma0 v s) "
"                      (implies (< (E s) (E sS)) (<= (E s) (E sT)) ) ) "
"                  :pattern ((inGamma0 v s) "
"                            (< (E s) (E sS)) (< (E sT) (E sS)) ) "
              " ) ) ) ) )";
#endif

  Z3_sort sorts[4] = { Var, Statement, Bool, Int };
  Z3_func_decl decls[5] = { E, InGamma[0], isMaxBefore, fStart, fInfinity};
  Z3ParseSMTLibString(funcDef, 4, sorts, 5, decls, "isMaxBefore");
#if 0
  /*
   * Fadi: I commented this out because it asserts that the variables
   * v2, sS, and sT abide by the constraint and not every application
   * of isMaxBefore. I replaced that by the Z3_parse_smtlib_string code aboce.
   */
  /*	implementation	*/
  Z3_symbol v2_name = Z3_mk_string_symbol(ctx, "v2");
  Z3_symbol sR_name = Z3_mk_string_symbol(ctx, "sR");
  Z3_symbol sS_name = Z3_mk_string_symbol(ctx, "sS");//TODO shouldn't SS be a bound variable?
  Z3_symbol sT_name = Z3_mk_string_symbol(ctx, "sT");

  Z3_ast v2 = Z3_mk_const(ctx, v2_name, Var);
  Z3_ast sR = Z3_mk_const(ctx, sR_name, Statement);
  Z3_ast sS = Z3_mk_const(ctx, sS_name, Statement);
  Z3_ast sT = Z3_mk_const(ctx, sT_name, Statement);

  Z3_ast E_sR = mk_unary_app(ctx, E, sR);
  Z3_ast E_sS = mk_unary_app(ctx, E, sS);
  Z3_ast E_sT = mk_unary_app(ctx, E, sT);
  Z3_ast InGamma_withArgs1 = mk_binary_app(ctx, InGamma, v2, sT);
  Z3_ast InGamma_withArgs2 = mk_binary_app(ctx, InGamma, v2, sR);

  Z3_ast constraints[3];
  constraints[0] = Z3_mk_eq(ctx, InGamma_withArgs1, True);
  constraints[1] = Z3_mk_le(ctx, E_sT, E_sS);

  Z3_ast temp1 = Z3_mk_lt(ctx, E_sR, E_sS);
  Z3_ast temp2 = Z3_mk_le(ctx, E_sR, E_sT);
  Z3_ast implies2 = Z3_mk_implies(ctx, temp1, temp2);
  Z3_ast implies1 = Z3_mk_implies(ctx, InGamma_withArgs2, implies2);

  Z3_sort FORALL_sorts[1];
  FORALL_sorts[0] = Statement;

  Z3_ast fxs[2];
  fxs[0] = Z3_mk_bound(ctx, 0, Statement);
  fxs[1] = InGamma_withArgs2;

  Z3_pattern FORALL_patterns;
  FORALL_patterns = Z3_mk_pattern(ctx, 2, fxs);

  Z3_symbol FORALL_decl_names[1];
  FORALL_decl_names[0] = sR_name;

  constraints[2] = Z3_mk_forall(ctx, 0, 1, &FORALL_patterns, 1, FORALL_sorts,
      FORALL_decl_names, implies1);

  Z3_ast constraint = Z3_mk_and(ctx, 3, constraints);

  Z3_ast isMaxBeforeArgs[3];
  isMaxBeforeArgs[0] = v2;
  isMaxBeforeArgs[1] = sS;
  isMaxBeforeArgs[2] = sT;

  Z3_ast isMaxBefore_Apply = Z3_mk_app(ctx, isMaxBefore, 3, isMaxBeforeArgs);

  /* assert that isMaxBefore (v2,sS,sT) = the and of the three constraints
   */
  Z3_ast isMaxBeforeDef = Z3_mk_eq(ctx, isMaxBefore_Apply, constraint);
  Z3_assert_cnstr(ctx, isMaxBeforeDef);
#endif

}
/*
 * s2i takes a statement and returns a number (Int) value
 * of the statement.
 * Z3: (declare-fun s2i (statement) Int)
 *
 *    The definition of this function happens by asserting its
 *    value with every statement in the traversal.
 */

void
PDTZ3Visitor::declareStatementToNumberValueFunction()
{

  s2i = new Z3_func_decl[CG.maxWhileDepth+1];

  for (unsigned int i = 0; i < CG.maxWhileDepth+1; i++){
    char s2iname[10];
    sprintf(s2iname, "s%d2i", i);

    Z3_symbol s2iSym = Z3_mk_string_symbol(ctx,s2iname );

    Z3_sort domain[1] = {ArrayOfStatements[i]};

    s2i[i] = Z3_mk_func_decl(ctx, s2iSym, 1, domain, Int);
    if ( i == 0)
        continue;
      /* 
       now asset that s2i[i](s) <=> forall j s2i[i-1](s[j])
       */
      const char * funcDefTemp = "(benchmark cg2z3 :formula "
        "(forall (s %s) (= (s%d2i s) "
        "(forall (i Int) ( s%d2i (select s i) ) ) ) ) )";
      char funcDef[1024];

      const char * aSI = Z3_sort_to_string(ctx, ArrayOfStatements[i]);
      sprintf(funcDef, funcDefTemp, aSI, i, i - 1);

      Z3_sort sorts[3] = {ArrayOfStatements[i - 1], 
          ArrayOfStatements[i], Int};

      Z3_func_decl decls[2] = { s2i[i-1], s2i[i]};

      Z3ParseSMTLibString(funcDef, 3, sorts, 2, decls, "s2i");
  }
}

/*
 Vs2i takes a variable v and a statement s and returns the
 number value of v at the time of execution of s.

 (define-fun Vs2i ((v Var) (s statement)) Int
(define-fun Vs2i ((v Var) (s Statement)) Int 
  (ite (= s Start)             (IV v) (
  (ite (> (E s) (E Infinity)) 0 (
  (ite (= (VAL v (E s)) Start) (IV v) (
                               s2i (VAL v (E s) ) ) ) ) ) ) ) )
 */
void
PDTZ3Visitor::declareAndDefineVariableStatementToInt()
{
  Z3_symbol Vs2i_name = Z3_mk_string_symbol(ctx, "Vs2i");
  Z3_sort Vs2i_domain[2];
  Vs2i_domain[0] = Var;
  Vs2i_domain[1] = Statement;
  Vs2i = Z3_mk_func_decl(ctx, Vs2i_name, 2, Vs2i_domain, Int);

#if 0
  Z3_ast v = Z3_mk_bound(ctx, 0, Var);
  Z3_ast s = Z3_mk_bound(ctx, 1, Statement);

//(s2i (VAL v (E s) ) )
  Z3_ast eS = mk_unary_app(ctx, E, s);
  Z3_ast valVeS = mk_binary_app( ctx, VAL, v, eS);
  Z3_ast s2iApp = mk_unary_app(ctx, s2i, valVeS);
//(IV v)
  Z3_ast ivV = mk_unary_app(ctx, IV, v);
//(= (VAL v (E s)) Start)  
  Z3_ast eS1 = mk_unary_app(ctx, E, s);
  Z3_ast valVeS1 = mk_binary_app( ctx, VAL, v, eS1);
  Z3_ast isStart = Z3_mk_eq(ctx, valVeS1, Start);

  /*(ite (= (VAL v (E s)) Start) (IV v) (
                                 s2i (VAL v (E s) ) ) )*/
  Z3_ast ite3 = Z3_mk_ite(ctx, isStart, ivV, s2iApp);

  // (ite (> (E s) (E Infinity)) 0 _ite3_
  Z3_ast eS2 = mk_unary_app(ctx, E, s);
  Z3_ast eInfinity = mk_unary_app(ctx, E, Infinity);
  Z3_ast eSgtInfinity = Z3_mk_gt(ctx, eS2, eInfinity);
  Z3_ast ite2 = Z3_mk_ite(ctx, eSgtInfinity, Zero, ite3);

  //(ite (= s Start)             (IV v) _ite2_
  Z3_ast sEqStart = Z3_mk_eq(ctx, s, Start);
  Z3_ast ivV1 = mk_unary_app(ctx, IV, v);
  Z3_ast ite1 = Z3_mk_ite(ctx, sEqStart, ivV1, ite2);

  Z3_sort sorts[2];
  sorts[0] = Var;
  sorts[1] = Statement;

  Z3_symbol names[2];
  /*
  names[0] = Z3_mk_string_symbol(ctx, makeName("v"));
  names[1] = Z3_mk_string_symbol(ctx, makeName("s"));
  */
  names[0] = Z3_mk_int_symbol(ctx, 0);
  names[1] = Z3_mk_int_symbol(ctx, 1);
  Z3_ast constraint = Z3_mk_forall(ctx, 0/*weight*/, 0/*numPatterns*/, 0/*patterns*/,//TODO: add patterns
          2, sorts, names, ite1);

  Z3_assert_cnstr(ctx, constraint);
  ////////////////////////
#else 
#if 0
  const char * funcDef = "(benchmark cg2z3 :formula"
(define-fun Vs2i ((v Var) (s Statement)) Int 
  (ite (= s Start)             (IV v) (
  (ite (> (E s) (E Infinity)) 0 (
  (ite (= (VAL v (E s)) Start) (IV v) ( 
                               s2i (VAL v (E s) ) ) ) ) ) ) ) )
#endif
  const char * funcDef = "(benchmark cg2z3 :formula "
     "(forall (v Var) (s Statement) "
     "(= (Vs2i v s) "
        "(ite (= s (fStart))             (IV v) ( "
        "(ite (> (E s) (E (fInfinity)))  0 ( "
        "(ite (= (VAL v (E s)) (fStart)) (IV v) ( "
                                       "s02i (VAL v (E s) ) ) ) ) ) ) ) ) ))";

  Z3_sort sorts[4] = {Var, Statement, Bool, Int};
  Z3_func_decl decls[7] = {Vs2i, fStart, IV, E, VAL, 
      fInfinity, s2i[0]};

  Z3ParseSMTLibString(funcDef, 4, sorts, 7, decls, "Vs2i");
#endif
}

void
PDTZ3Visitor::setup()
{
  config = Z3_mk_config();
/*
(set-option PULL_NESTED_QUANTIFIERS true)
(set-option MODEL_COMPACT true)
(set-option MBQI true)
(set-option enable-cores)
 */
Z3_set_param_value(config, "MODEL", "true");
Z3_set_param_value(config, "PULL_NESTED_QUANTIFIERS", "true");
Z3_set_param_value(config, "MODEL_COMPACT", "true");
Z3_set_param_value(config, "MBQI", "true");
//Z3_set_param_value(config, "enable-cores", "true");
/*
   to get the unsat-core use:
   result = Z3_check_assumptions(ctx, 4, assumptions, &m, &proof, &core_size, core);
*/

  //Z3_set_param_value(config, "MODEL", "true");
  //Z3_set_param_value(cfg, "PROOF_MODE", "2");
  ctx = Z3_mk_context(config);
  Z3_trace_to_stderr(ctx);

  /* Var, Statement, Int, Bool, Start, Infinity, True, False, Zero*/
  buildTypesAndConstants();
  cout << "check 1" << endl;
  check();

  /* E: Statement -> Int */
  declareExecutionTimeFunction();
  cout << "check 2" << endl;
  check();

  /* inGamma: (Var Statement) -> bool */
  declareInGamma();
  cout << "check 3" << endl;
  check();

  /* declare and define isMaxBefore */
  declareAndDefineIsMaxBefore();
  cout << "check 4" << endl;
  check();

  /* Val: (Var Int) -> Statement */
  declareAndDefineVal();
  cout << "check 5" << endl;
  check();

  /* TODO: s0 = Start & implement forall
   pattern is statment ~= start */

  /* s2i: (Statement) -> Int*/
  declareStatementToNumberValueFunction();
  cout << "check 6" << endl;
  check();

  /*
   * Vs2i: (Var Statement) -> Int
   */
  declareAndDefineVariableStatementToInt();
  cout << "check 7" << endl;
  check();
}

Z3_ast
PDTZ3Visitor::mk_var(Z3_context ctx, const char * name, Z3_sort ty)
{
  Z3_symbol s = Z3_mk_string_symbol(ctx, name);
  Z3_ast v = Z3_mk_const(ctx, s, ty);
  return v;
}

Z3_sort
PDTZ3Visitor::makeArrayOfStatementsSort(int dimension)
{
  if (dimension == 0)
    ArrayOfStatements[0] = Statement;
  else
    ArrayOfStatements[dimension] = Z3_mk_array_sort(ctx, Int,
        makeArrayOfStatementsSort(dimension - 1));

  return ArrayOfStatements[dimension];
}

Z3_ast
PDTZ3Visitor::makeArrayOfStatements(int dimension, const char * name)
{
  Z3_sort sort = makeArrayOfStatementsSort(dimension);
  Z3_ast statementArray = mk_var(ctx, name, sort);
  return statementArray;
}

Z3_ast
PDTZ3Visitor::mk_unary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x)
{
  Z3_ast args[1] =
    { x };
  return Z3_mk_app(ctx, f, 1, args);
}

Z3_ast
PDTZ3Visitor::mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y)
{
  Z3_ast args[2] =
    { x, y };
  return Z3_mk_app(ctx, f, 2, args);
}

Z3_ast
PDTZ3Visitor::makeStatement(const char * name)
{
  Z3_symbol S_name = Z3_mk_string_symbol(ctx, name);
  Z3_ast S = Z3_mk_const(ctx, S_name, Statement);
  return S;
}

void
PDTZ3Visitor::assertOrder(Z3_ast s1, Z3_ast s2)
{
  Z3_ast E1 = mk_unary_app(ctx, E, s1);
  Z3_ast E2 = mk_unary_app(ctx, E, s2);
  Z3_ast constraint = Z3_mk_lt(ctx, E1, E2);
  Z3_assert_cnstr(ctx, constraint);
}
void
PDTZ3Visitor::assertConditionalOrder(Z3_ast condition, Z3_ast target,
    Z3_ast _if, Z3_ast _else)
{
  Z3_ast E1 = mk_unary_app(ctx, E, _if);
  Z3_ast E2 = mk_unary_app(ctx, E, _else);
  Z3_ast Et = mk_unary_app(ctx, E, target);

  Z3_ast ite = Z3_mk_ite(ctx, condition, E1, E2);
  Z3_ast constraint = Z3_mk_gt(ctx, Et, ite); //TODO: shouldn't it be E(ife) ?
  Z3_assert_cnstr(ctx, constraint);
}

Z3_ast
PDTZ3Visitor::makeBound(Z3_sort t, Z3_symbol & vName){
    Z3_ast boundVar = Z3_mk_bound(ctx,  boundCounter, t);
    vName =  Z3_mk_int_symbol(ctx, boundCounter);
    boundCounter++;
    return boundVar;
}

///////////////////////////////////////////////////////////////////////////////////////////////

PDTZ3Visitor::PrepQuantifier::PrepQuantifier(unsigned int aMaxWhileDepth) :
  maxWhileDepth(aMaxWhileDepth), weight(0), numPatterns(0), numDecls(0),
      body(0)
{
  patterns = new Z3_pattern[MAXPATTERNS];

  sorts = new Z3_sort[maxWhileDepth+1];
  declNames = new Z3_symbol[maxWhileDepth+1];
  iterators = new Z3_ast[maxWhileDepth+1];

  for (unsigned int i = 0; i < maxWhileDepth+1; i++)
    {
      sorts[i] = 0;
      declNames[i] = 0;
      iterators[i] = 0;
    }
  for (unsigned int i = 0; i < MAXPATTERNS; i++)
      patterns[i] = 0;
}

PDTZ3Visitor::PrepQuantifier::~PrepQuantifier()
{
  delete[] patterns;
  delete[] sorts;
  delete[] declNames;
  delete[] iterators;
}

void
PDTZ3Visitor::PrepQuantifier::clear()
{
  weight = 0;
  numPatterns = 0;
  numDecls = 0;
  body = 0;

  for (unsigned int i = 0; i < maxWhileDepth+1; i++)
    {
      patterns[i] = 0;
      sorts[i] = 0;
      declNames[i] = 0;
      iterators[i] = 0;
    }
}

Z3_ast
PDTZ3Visitor::PrepQuantifier::makeForall(PDTZ3Visitor & ZV)
{
  return Z3_mk_forall(ZV.ctx, weight, numPatterns, patterns, numDecls, sorts,
      declNames, body);
}

Z3_ast
PDTZ3Visitor::PrepQuantifier::makeExists(PDTZ3Visitor & ZV)
{
  return Z3_mk_exists(ZV.ctx, weight, numPatterns, patterns, numDecls, sorts,
      declNames, body);
}

void
PDTZ3Visitor::PrepQuantifier::prepareIterators(PDTZ3Visitor & ZV)
{
  if (!ZV.currentNode->isStatement())
    return;
  PDTStatement * stmnt = dynamic_cast<PDTStatement *> (ZV.currentNode);
  if (stmnt == NULL)
    return;

  numDecls = stmnt->depth;
  for (unsigned int i = 0; i < numDecls; i++)
    {
      sorts[i] = ZV.Int;
      iterators[i] = ZV.makeBound(ZV.Int,declNames[i]);
    }
}

Z3_ast
PDTZ3Visitor::PrepQuantifier::makeSelect(PDTZ3Visitor & ZV,
    Z3_ast arrOfStatements)
{
  Z3_ast ret = arrOfStatements;
  for (unsigned int i = 0; i < numDecls; i++)
    {
      ret = Z3_mk_select(ZV.ctx, ret, iterators[i]);
    }
  return ret;
}

#ifdef YICES_DEF
/*
 utility function to convert a string to a character array
 */
char * PDTYicesVisitor::stringToCharArray(string s)
  {
    return (char*)s.c_str();
  }

/*
 utility function to convert a constant character array to a character array
 */
char * PDTYicesVisitor::constCharToChar(const char * cArray)
  {
    return const_cast<char *> (cArray);
  }
/*
 function that takes a string containing the yices command, executes it, and returns the result
 */
int PDTYicesVisitor::writeToYices(string statement)
  {
    char *temp=new char[statement.length()+1];
    strcpy(temp,statement.c_str());
    int i=yicesl_read(lctx,temp);
    if (i==1)
    cout<<statement<<endl;
    //cout<<yicesl_get_last_error_message()<<"\n";

    return i;
  }
/*
 function that takes a char array containing the yices command, executes it, and returns the result
 */
int PDTYicesVisitor::writeToYices( char * statement)
  {

    int i=yicesl_read(lctx,statement);
    if (i==1)
    cout<<statement<<endl;
    //cout<<yicesl_get_last_error_message()<<"\n";

    return i;
  }
/*
 function that takes a constant char array containing the yices command, executes it, and returns the result
 */
int PDTYicesVisitor::writeToYices(const char * statement)
  {
    char *temp=new char[strlen(statement)+1];
    strcpy(temp,statement);
    int i=yicesl_read(lctx,temp);
    if (i==1)
    cout<<statement<<endl;
    //cout<<yicesl_get_last_error_message()<<"\n";

    return i;
  }

/*
 constructor for the PDTYicesVisitor class that takes a PDTCodeGraph and does the initializations and executes
 the first statements in yices
 */
PDTYicesVisitor::PDTYicesVisitor(PDTCodeGraph &CG)
  {
    ctx=yices_mk_context();
    firstTime=true;
    assignTarget=false;
    ifCondition=false;
    lctx= yices_get_lite_context(ctx);
    writeToYices("(set-evidence! true)");
    writeToYices("(set-verbosity! 3)");
    writeToYices("(define-type _exp)");
    writeToYices("(define-type _i (-> int int))");
    writeToYices("(define-type _b (-> int bool))");
    writeToYices("(define _EC::(-> _exp int))");
    writeToYices("(define _ival::(-> _exp int))");
    writeToYices("(define _bval::(-> _exp bool))");
    writeToYices("(define e0::_exp)");
    writeToYices("(define e_end::_exp)");
    writeToYices("(assert (= (_EC e0) 0))");

    currentID=0;
    previousID=-1;
    currentAssertion="";

  }
/*
 prints the execution counter
 */
void PDTYicesVisitor::ECPrinter()
  {
    currentAssertion.append(" (_EC e").append(inttochar(previousID)).append(" ) ");

  }
/*
 appends one paranthesis to the current assertion statement
 */
void PDTYicesVisitor::appendParan()
  {
    currentAssertion.append(")");
  }

/*
 updates previousID to currentID, increments currentID, and defines currentID in yices
 */
void PDTYicesVisitor::updateIDs(bool assertGreater)
  {
    string statement="";
    previousID=currentID;
    currentID++;
    char input[100];
    sprintf(input,"(define e%d::_exp)",currentID);
    writeToYices(input);
    /* assertGreater is false when we have an if statement where the assertion of greater than is done conditionally
     i.e. depending on the if content
     */
    if (assertGreater)
      {
        sprintf(input,"(assert+ (> (_EC e%d) (_EC e%d)))",currentID,previousID);
        writeToYices(input);
      }

  }
/*
 extracts the name from PDTNumVar, defines a variable in yices and defines a generic
 variable (maybe this last step isn't needed)
 */
int PDTYicesVisitor::declareNumVar(PDTNode * me)
  {
    string varNameTemp=((PDTNumVar*)me)->getName();
    char * varName=stringToCharArray(varNameTemp);
    char * statement= new char[strlen(varName)+200]; //this can fail if the variable is too long
    sprintf(statement,"(define %s::_i)",varName);
    int i=writeToYices(statement);
    if (i!=0)
      {
        sprintf(statement,"(define %s_generic::_i)",varName);
        writeToYices(statement);
        sprintf(statement,"(assert+ (= %s_generic (lambda (i::int) (if (and (> i 0) (< i (_EC e_end))) (%s_generic (- i 1)) (%s_generic i)))))",varName,varName,varName);
        writeToYices(statement);
      }
    return i;
  }
/*
 extracts the name from booleans, defines a variable in yices
 */
int PDTYicesVisitor::declareBoolVar(PDTNode * me)
  {
    string statement="(define ";
    statement.append(((PDTNumVar*)me)->getName()).append("::(-> int bool))");

    return writeToYices(statement);

  }

/*
 This function is executed before children are traversed
 */
bool PDTYicesVisitor::pre(PDTNode * me)
  {
    NodeTypeEnum type =me->getType();
    //	if ( (type==PDTAnd_Em) || (type==PDTOr_Em) || (type==PDTEqualBool_Em) || (type==PDTNotEqualBool_Em) || (type==PDTEqualNum_Em)
    //		|| (type==PDTNotEqualNum_Em) || (type==PDTGreaterThan_Em) || (type==PDTGreaterThanEqual_Em) || (type==PDTLessThan_Em)
    //		|| (type==PDTLessThanEqual_Em_Em))


    string statement="";
    switch (type)
      {
        case PDTNumVar_Em:
        if (assignTarget)
        currentAssertion.append("(_ival e").append(inttochar(currentID)).append(") ");
        else
        currentAssertion.append("(").append(((PDTNumVar*)me)->getName());
        declareNumVar(me);
        break;

        case PDTNumConstInt_Em:
        currentAssertion.append(inttochar(((PDTNumConstInt *)me)->getValue()));
        break;
        case PDTNumConstDbl_Em:
        currentAssertion.append(doubletochar(((PDTNumConstDbl *)me)->getValue()));
        break;
        case PDTBoolVar_Em:
        if (assignTarget) //in case of boolean assignment or if condition
        currentAssertion.append("(_bval e").append(inttochar(currentID)).append(") ");
        else
        currentAssertion.append("(").append(((PDTBoolVar*)me)->getName());

        declareBoolVar(me);
        break;
        case PDTBoolConst_Em:
        if(((PDTBoolConst *)me)->getValue()==false)
        currentAssertion.append("false");
        else
        currentAssertion.append("true");
        break;
        case PDTAdd_Em:
        currentAssertion.append("(+ ");
        break;
        case PDTSubt_Em:
        currentAssertion.append("(- ");
        break;
        case PDTMult_Em:
        currentAssertion.append("(* ");
        break;
        case PDTDiv_Em:
        currentAssertion.append("(/ ");
        break;
        case PDTMod_Em:
        currentAssertion.append("(mod ");
        break;
        case PDTAssign_Em://////////
        updateIDs(true);
        assignTarget=true;
        currentAssertion="(assert+ (= ";
        break;
        case PDTWhile_Em://///////////
        cout<<"while( ";
        break;
        case PDTIfElse_Em://///////
        updateIDs(true);
        ifCondition=true;
        ifHelper.push(currentID);//push the if condition expression id
        currentAssertion="(assert+ (= (_bval e";
        currentAssertion.append(inttochar(currentID)).append(") ");
        break;
        case PDTAnd_Em:
        currentAssertion.append("(and ");
        break;
        case PDTOr_Em:
        currentAssertion.append("(or ");
        break;
        case PDTLessThan_Em:
        currentAssertion.append("(< ");
        break;
        case PDTGreaterThan_Em:
        currentAssertion.append("(> ");
        break;
        case PDTLessThanEqual_Em:
        currentAssertion.append("(<= ");
        break;
        case PDTGreaterThanEqual_Em:
        currentAssertion.append("(>= ");
        break;
        case PDTEqualNum_Em:
        currentAssertion.append("(= ");
        break;
        case PDTEqualBool_Em:
        currentAssertion.append("(= ");
        break;
        case PDTNotEqualNum_Em:
        currentAssertion.append("(/= ");
        break;
        case PDTNotEqualBool_Em:
        currentAssertion.append("(/= ");
        break;
        case PDTNeg_Em://///////////
        cout<<"-";
        break;
        case PDTNot_Em:///////
        break;
        case PDTListOfStatements_Em://///////////
        ;
        break;
        default:
        ;
      }
    return true;
  }

/*
 This function is executed between each two children traversal
 */
bool PDTYicesVisitor::in(PDTNode * me, PDTNode* child, unsigned int i)
  {
    NodeTypeEnum type =me->getType();
    char tempIf[200];
    int ifCond;

    switch (type)
      {
        /*	case (PDTNumVar_Em||PDTNumConstInt_Em||PDTNumConstDbl_Em||PDTBoolVar_Em||PDTBoolConst_Em):
         break;
         */
        case PDTNumConstInt_Em:
        break;
        case PDTNumVar_Em:
        break;
        case PDTAdd_Em:
        break;
        case PDTSubt_Em:

        break;
        case PDTMult_Em:

        break;
        case PDTDiv_Em:

        break;
        case PDTMod_Em:

        break;
        case PDTAssign_Em:
        //(yicesHelper[me->getId()]).args[i]=(yicesHelper[child->getId()]).expr;
        if (i==0)
        //currentAssertion.append(" (_EC e").append(inttochar(currentID)).append(" ))");
        assignTarget=false;
        break;
        case PDTWhile_Em://///////////
        if (i==0)
        cout<<") {\n";
        break;
        case PDTIfElse_Em:////
        if (i==0)
          {
            ifCondition=false;
            currentAssertion.append("))");
            //	cout<<currentAssertion<<endl;
            writeToYices(currentAssertion);
            updateIDs(false);
            sprintf(tempIf,"(assert+ (= true (if (_bval e%d) (= (_EC e%d) (_EC e%d)) (> (_EC e%d) (_EC e_end) ) ) ))",
                previousID,currentID,previousID,currentID);
            writeToYices(tempIf);
          }
        else if (i==1)
          {
            updateIDs(false);
            ifCond=ifHelper.top();
            sprintf(tempIf,"(assert+ (= true (if (not (_bval e%d)) (= (_EC e%d) (_EC e%d)) (> (_EC e%d) (_EC e_end) ) ) ))",
                ifCond,currentID,ifCond,currentID);
            writeToYices(tempIf);
            ifHelper.push(previousID);//push the last statement id in if block
          }

        break;
        case PDTAnd_Em:

        break;
        case PDTOr_Em:

        break;
        case PDTLessThan_Em:

        break;
        case PDTGreaterThan_Em:

        break;
        case PDTLessThanEqual_Em:

        break;
        case PDTGreaterThanEqual_Em:

        break;
        case PDTEqualNum_Em:

        break;
        case PDTEqualBool_Em:

        break;
        case PDTNotEqualNum_Em:

        break;
        case PDTNotEqualBool_Em:

        break;
        case PDTNeg_Em://///////////
        break;
        case PDTNot_Em:
        //	(yicesHelper[me->getId()]).args[i]=(yicesHelper[child->getId()]).expr;
        break;
        case PDTListOfStatements_Em://///////////
        ;
        break;

        case PDTProp_Em:
        //	(yicesHelper[me->getId()]).expr=(yicesHelper[child->getId()]).expr;
        break;

        default:
        ;
      }
    return true;

  }
/*
 This function is executed after traversing the children
 */
bool PDTYicesVisitor::post(PDTNode * me)
  {
    NodeTypeEnum type =me->getType();
    char tempIf[200];
    int lastInIf,ifCond;
    switch (type)
      {
        /*	case (PDTNumVar_Em||PDTNumConstInt_Em||PDTNumConstDbl_Em||PDTBoolVar_Em||PDTBoolConst_Em):
         break;
         */
        case (PDTNumVar_Em):
        if (!assignTarget)
          {
            ECPrinter();
            appendParan();
          }
        break;
        case (PDTBoolVar_Em):
        if (!assignTarget)
          {
            ECPrinter();
            appendParan();
          }
        break;
        case PDTNumConstInt_Em:
        break;
        case PDTAdd_Em:
        appendParan();
        break;
        case PDTSubt_Em:
        appendParan();
        break;
        case PDTMult_Em:
        appendParan();
        break;
        case PDTDiv_Em:///////////
        appendParan();
        break;
        case PDTMod_Em://///////
        appendParan();
        case PDTAssign_Em:///////
        appendParan();appendParan();
        firstTime=false;
        writeToYices(currentAssertion);
        break;
        case PDTWhile_Em:////////
        //cout<<"}\n";
        break;
        case PDTIfElse_Em://////
        //appendParan();
        //	cout<<")";
        updateIDs(false);
        lastInIf=ifHelper.top();
        ifHelper.pop();
        ifCond=ifHelper.top();
        ifHelper.pop();
        sprintf(tempIf,"(assert+ (= (_EC e%d) (if (_bval e%d) (_EC e%d) (_EC e%d) )))",
            currentID,ifCond,lastInIf,previousID);

        writeToYices(tempIf);
        break;
        case PDTAnd_Em:
        appendParan();
        break;
        case PDTOr_Em:
        //	(yicesHelper[me->getId()]).expr=yices_mk_or(ctx,(yicesHelper[me->getId()]).args,2);
        break;
        case PDTLessThan_Em:
        appendParan();
        break;
        case PDTGreaterThan_Em:
        appendParan();
        break;
        case PDTLessThanEqual_Em:
        appendParan();
        break;
        case PDTGreaterThanEqual_Em:
        appendParan();
        break;
        case PDTEqualNum_Em:
        appendParan();
        break;
        case PDTEqualBool_Em:
        appendParan();
        break;
        case PDTNotEqualNum_Em:
        appendParan();
        break;
        case PDTNotEqualBool_Em:
        appendParan();
        break;
        case PDTNeg_Em://///////
        break;

        case PDTNot_Em:
        //	(yicesHelper[me->getId()]).expr=yices_mk_not(ctx,(yicesHelper[me->getId()]).args[0]);
        break;

        case PDTListOfStatements_Em://///////
        break;
        case PDTProp_Em:
        //	yices_assert(ctx, (yicesHelper[me->getId()]).expr);
        //	yices_pp_expr((yicesHelper[me->getId()]).expr);
        break;
        default:
        ;
      }
    return true;
  }
#endif

